\newcommand{\PRE}{P^\ast}
\newcommand{\POST}{P_\ast}
Successful application of ROP based attacks requires gadgets to be detected and classified.
Intuitively, this means that gadgets must be found within a binary and then identified based on their operational semantics.
Operational semantics provide a meaning for a computer program in a mathematically rigorous way.
Manual disassembly and inspection is the most obvious and time consuming method for detection and classification.
However, our goal is to demonstrate mechanically generated ROP based attacks given a binary and a ROP payload description (discussed in Section~\ref{sec:input_language}).
In this section, the mechanical detection and classification of gadgets is discussed.

\subsection{Binary Analysis Platform}
\label{sec:bap}


The Binary Analysis Platform (BAP) \cite{BAPmanual} is a tool designed for formal reasoning about binaries.
The tool is maintained by David Brumley at Carnegie Mellon University.
Its main focus is to facilitate analysis of binary code, in the absence of source, in a high-fidelity manner.
Our tools rely on BAP (version $0.6$) for lifting (described below) and control flow graph generation.

\textit{Lifting} disassembles and then translates a binary into the BAP Intermediate Language (BIL).
This is accomplished using the BAP \texttt{toil} tool.
Each instruction in the disassembled binary is translated into a BIL instruction.
Besides normalizing certain instructions, BIL instructions provide address and effect information.
Figure \ref{fig:bil_instruction} shows a sample BIL instruction.

\begin{figure*}
%%\begin{minipage}{0.53\textwidth}
\begin{Verbatim}[frame=lines]
addr 0x804829e @asm "add    $0x1d57,%ebx"
label pc_0x804829e
T_t1:u32 = R_EBX:u32
T_t2:u32 = 0x1d57:u32
R_EBX:u32 = R_EBX:u32 + T_t2:u32
R_CF:bool = R_EBX:u32 < T_t1:u32
R_AF:bool = 0x10:u32 == (0x10:u32 & (R_EBX:u32 ^ T_t1:u32 ^ T_t2:u32))
R_OF:bool = high:bool((T_t1:u32 ^ ~T_t2:u32) & (T_t1:u32 ^ R_EBX:u32))
R_PF:bool =
  ~low:bool(R_EBX:u32 >> 7:u32 ^ R_EBX:u32 >> 6:u32 ^ R_EBX:u32 >> 5:u32 ^
            R_EBX:u32 >> 4:u32 ^ R_EBX:u32 >> 3:u32 ^ R_EBX:u32 >> 2:u32 ^
            R_EBX:u32 >> 1:u32 ^ R_EBX:u32)
R_SF:bool = high:bool(R_EBX:u32)
R_ZF:bool = 0:u32 == R_EBX:u32
\end{Verbatim}
%% $
\caption{An example BIL instruction. The first line is the normalized instruction and address. 
The rest of the BIL instruction define this instructions effects. \texttt{R\_EBX:u32 = R\_EBX:u32 + T\_t2:u32} describes the actual addition operation. 
The rest of the equations describe flags that may be set on overflow, underflow, etc. }
\label{fig:bil_instruction}
%%\end{minipage}
\end{figure*}

The BAP \texttt{iltrans} tool provides a mechanism to transform BIL.
Our tool relied on an abstract syntax tree (AST) graph representation.
This transformation creates a node for each BIL instruction and places an edge between any two nodes that may be executed in sequence.

Finally, BAP also includes the \texttt{topredicate} tool.
\texttt{topredicate} takes a set of BIL instructions and a formula.
The formula is negated and counter-examples to validity are searched for.
This particular tool contains many options.
Our tool makes heavy use of the symbolic execution(\texttt{-fse-bfs}) option.

\subsection{Detection}
\label{sec:det}
In the pedantic sense, gadget detection is a misnomer.
Recall that a gadget is a list of instructions proceeded by a \texttt{ret}.
Thus, finding gadgets only requires finding \texttt{ret}.
This says nothing of the semantic characteristics and is a useless endeavor.

Potential gadget detection would better reflect the notion of this stage.
A \emph{potential gadget} is the term used for a non-empty sequential list of non-control flow altering instructions proceeded by a \texttt{ret}. 
Figure \ref{fig:ex_potential_gadget} is such a potential gadget.
Note that by the definition of a potential gadget, potential gadgets may contain potential gadgets.
This becomes important during gadget classification and will be discussed in Section \ref{sec:class}.
For the moment, it is sufficient to say that any potential gadget of instruction size $n>1$ (the definition requires there be at least one instruction and a \texttt{ret}) contains $n-2$ potential gadgets.

\begin{figure}
\centering
\begin{Verbatim}[frame=lines]
1: add $0x4,%esp
2: pop %ebx
3: pop %ebp
4: ret
\end{Verbatim}
%% The following line will correct an emacs syntax highlighting issue.
%% $
\caption{A potential gadget example. Each instruction is prefixed with an index for ease of reference.}
\label{fig:ex_potential_gadget}
\end{figure}

A single binary file may contain many potential gadgets.
This set is referred to as a potential gadget set.
Potential gadget sets are generated via a three step process.
First, the BAP tool responsible for lifting binaries into the BAP intermediate language is run.
The second step uses this file as input into the BAP tool that generates a BIL instruction control flow graph.
The final step involves our tool for generating potential gadgets.
This tool does a reverse (with respect to execution flow) search from each \texttt{ret} in a text file using the BIL instruction control flow graph.
When the search encounters a control flow altering instruction (e.g., \texttt{jmp}) the search is complete, a potential gadget is identified, and the next \texttt{ret} in the BIL instruction control flow graph is examined.
When there are no more \texttt{ret}s in the binary file to be examined, detection is complete.

The caveat to this potential gadget set generation relates to the handling of interrupts. (In particular, \texttt{int 0x80}).
The version of BAP used did not support reasoning over interrupt instructions.
Our solution was to simply replace these instructions with \texttt{nop} and note that gadget as one containing an interrupt.
A discussion of the benefits of this workaround is provided in the next section.

\subsection{Classification} 
\label{sec:class}

Gadget classification analyzes each potential gadget in a potential gadget set to determine if it meets the operational semantics criteria (hereafter referred to as behavior) for a desired gadget.
Each potential gadget that has such behavior is classified accordingly.
Only then are they referred to as gadgets.

Classifications are not mutually exclusive; it is possible for a potential gadget have multiple behaviors.
Thus, a single potential gadget may be classified as multiple different gadgets.

It must be known what a gadget does and, equally importantly, does not do for a gadget to be used correctly in a ROP payload.
If a desired gadget behavior is to increment the value in \texttt{\%eax}, the following gadget should not invalidate this behavior.
Behavior is determined via a post-condition formula considered under the output state of a potential gadget, assuming a precondition.
Intuitively, each behavior classification goes as follows, ``If the pre-condition is some set of variables that are equal to the state of the process before a gadget is executed, then my post-condition should be true after the gadget is executed.''

Formally, behavior is defined by the triple $(N,\PRE,\POST)$ where $N$ is some human description of the behavior, $\PRE$ is the precondition, and $\POST$ is the post-condition.
For such a triple, $N$ loosely follows the context specific grammar defined in Figure~\ref{fig:gagdet_type_naming_scheme}.
The unary operator $\ ^*$ looks up the value at the memory address contained within the register and $NOCHANGE$ indicates a list of registers that should not change. By way of example, consider the name\\ \texttt{EBX:=*ESP\_ESP:=ESP+8\_NOCHANGE:EAX}.
The behavior of a gadget associated with this name should be clear.

The component $\PRE$ and $\POST$ are specified via a propositional formula with a term language that supports common low-level process operations such as shift, memory lookup, addition, boolean operations, etc.
The grammar for the propositional formula can be found in \cite{BAPmanual}.
Examples of what $\PRE$ and $\POST$ might look like can be found in Section \ref{sec:detclassexample}.

\begin{figure}
{\setlength\tabcolsep{4pt}
\begin{tabular}{lcl}
  $N$ & ::= & $STMTS$\\
  $STMTS$ & ::= & $STMT$'\_'$STMTS$ | $STMT$ | $\epsilon$ \\
  $STMT$ & ::= & $EXPR$':='$EXPR$ \\
         & | & $CONSTRAINT$ | '$INT80$'\\
  $EXPR$ & ::= & $REG$ | $\ ^{\ast}REG$ | $EXPR\ OP\ EXPR$\\
        & | & '[0-9]+' \\
  $OP$ & ::= & '$+$' | '$-$' \\
  $REG$ & ::= & '$EAX$' | '$EBX$' | '$ECX$'\\
        &  | & '$EDX$' | '$ESP$'\\
  $CONSTRAINT$ & ::= & '$NOCHANGE:$' $LIST$\\
  $LIST$ & ::= & $REG$ | $REG$','$LIST$ \\
\end{tabular}}
\caption{The context free grammar that is loosely used to specify human readable names for gadget behaviors.}
\label{fig:gagdet_type_naming_scheme}
\end{figure}

The output state of a potential gadget is discovered by interpreting the operational semantics of each BIL instruction in the potential gadget as a set of constraints.
This is the symbolic execution process discussed in Section \ref{sec:bap}.
Due to this, the actual fidelity of gadget classification is determined by the adequacy of BIL instruction operational semantics encoding and the correctness of the symbolic execution process.
We assume BAP provides a sufficiently adequate encoding and correct symbolic execution process for our purposes.

In Section \ref{sec:det}, it was mentioned that potential gadgets may contain 
potential gadgets.
This becomes of importance during classification.
Consider Figure \ref{fig:ex_potential_gadget} again.
Suppose gadgets with a behavior of not modifying \texttt{\%ebx} were desired.
Then the potential gadget composed of instruction $1$ through $4$ would not
be a potential gadget, similarly with the potential gadget composed of instruction $2$ through $4$.
The potential gadget composed of instruction $3$ and $4$ would satisfy this behavior; jumping to the address of this instruction would not alter \texttt{\%ebx}.
For completeness of this example, consider the instruction $4$; this is not a potential gadget by definition.
This example demonstrates the importance of defining potential gadgets in this way.

\subsection{Concrete Example}
\label{sec:detclassexample}
This section will demonstrate gadget detection and classification.
When generating ROP payload, source code is not required.
However, to make the process of gadget detection and classification transparent the trivial program in Figure \ref{fig:ex_detclass_c} will be used.

Taken in whole, this program is not particularly interesting.
However, consider what must be done to detect and classify a gadget with the name \texttt{EBX:=*ESP\_ESP:=ESP+4} assuming the this program is compiled via \texttt{gcc example.c}.
First the binary is lifted and a BIL instruction control flow graph generated.
This step is performed exclusively by BAP and a brief description of this operation can be found in Section \ref{sec:bap}.
Then the potential gadget set must be constructed.
As this binary is an excitable there is a non-trivial amount of code added to what we see in Figure \ref{fig:ex_detclass_c} by the compiler.
Our tool generates a potential gadget set of size $32$.

At this point, detection is complete and classification can begin.
A classification triple is selected.
For this example, there is only one triple to choose and can be found in Figure \ref{fig:triple}.
$\PRE$ and $\POST$ may be intuitively interpreted as ``there exists an $S$ that is equal to \texttt{\%esp} before the gadget is executed'' and  as ``the memory at address $S$ is equal to \texttt{\%ebx} and \texttt{\%esp} has been incremented by $4$ after the gadget is executed''.
$\PRE$ is then prepended to the potential gadget and $\POST$ is solved for using the BAP symbolic execution engine.
Essentially, this is done by taking the negation of $\POST$ and finding a contradiction.
Symbolic execution will return three possible outcomes:
\begin{enumerate}
\item \textit{Valid}. That is, the negation of $\POST$ with $\PRE$ prepended to the potential gadget is always true. This means that this potential gadget \textbf{does not} exhibit the behavior this triple describes.
\item \textit{Invalid with a model}. That is, the negation of $\POST$ with $\PRE$ prepended to the potential gadget can be false under a specific model. This means that this potential gadget \textbf{does} exhibit the behavior but possibly only under the provided model. The model may specify register and memory values. Our tools did not use these result due to the complexity in composing gadgets with models.
\item \textit{Contradiction}. That is, the negation of $\POST$ with $\PRE$
prepended to the potential gadget will be false in all cases. This means that this potential gadget \textbf{is} a gadget that exhibits the behavior described by the triple.
\end{enumerate}

For this example, symbolic execution results in a contradiction.
That is, a gadget was found with the behavior describe by the triple in Figure \ref{fig:triple}.
While this may seem obvious to the trained expert, this is not a trivial task to automate.
Not only is \texttt{\%ebx} set through an intermediate register (\texttt{\%eax}) pointer dereference, but that register was modified before the final assignment was complete.
Considering that binaries may have thousands of potential gadgets, manual review is labor intensive making an automated utility preferred.

\begin{figure}
\centering
\begin{Verbatim}[frame=lines]
void main() { a(); }
void a() {
  __asm__
  (
  "mov %esp,%eax\n"
  "nop\n"
  "xor %ecx,%edx\n"
  "add 0x01,%eax\n"
  "sub 0x01,%eax\n"
  "mov (%eax),%ebx\n"
  "ret\n"
   );
}
\end{Verbatim}
\caption{The program used as an example in Section \ref{sec:detclassexample}.}
\label{fig:ex_detclass_c}
\end{figure}

\begin{figure}
$N$ = \texttt{EBX:=*ESP\_ESP:=ESP+4}\\
$\PRE$ = \texttt{S:u32 = R\_ESP:u32}\\
$\POST$ = \texttt{mem:?u32[S:u32,e\_little]:u32 == R\_EBX:u32 \& R\_ESP:u32 == S:u32 + 4:u32}\\
\caption{ The classification triple used in the example in Section \ref{sec:detclassexample}.}
\label{fig:triple}
\end{figure}

The final step of gadget detection and classification is to output the gadgets.
The output can be seen in Figure \ref{fig:detclass_out}.
Verification that this address is correct can be found in Figure \ref{fig:objdump_a}.

\begin{figure}
\begin{Verbatim}[frame=lines]
BEGIN
        address="0x80483c6"
        type="EBX:=*ESP_ESP:=ESP+4"
END
\end{Verbatim}
\caption{A gadget from a compiled binary of the example file in Figure \ref{fig:ex_detclass_c} classified by the triple in Figure \ref{fig:triple}. The address is where that gadget starts in the program and type is the classification of the gadget.}
\label{fig:detclass_out}
\end{figure}

\begin{figure}
\begin{Verbatim}[frame=lines]
080483c3 <a>:
 80483c3: 55                      push   %ebp
 80483c4: 89 e5                   mov    %esp,\%ebp
 80483c6: 89 e0                   mov    %esp,%eax
 80483c8: 90                      nop
 80483c9: 31 ca                   xor    %ecx,%edx
 80483cb: 03 05 01 00 00 00       add    0x1,%eax
 80483d1: 2b 05 01 00 00 00       sub    0x1,%eax
 80483d7: 8b 18                   mov    (%eax),%ebx
 80483d9: c3                      ret    
 80483da: 5d                      pop    %ebp
 80483db: c3                      ret    
\end{Verbatim}
\caption{The \texttt{objdump} output for function \texttt{a} from disassembling a compiled binary of \ref{fig:ex_detclass_c}}
\label{fig:objdump_a}
\end{figure}
